Nuprl Lemma : p-first-singleton
11,40
postcript
pdf
A
,
B
:Type,
f
:(
A
(
B
+ Top)). p-first([
f
]) =
f
latex
ProofTree
Definitions
f
(
a
)
,
p-first(
L
)
,
Top
,
left
+
right
,
s
=
t
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
Type
origin
A, B:Type, f:(A
(B + Top)). p-first([f]) = f
A, B:Type, f:(A(B + Top)). p-first([f]) = f
B(x)x:A. B(x)